M.rframe(A.effect f of k on y)
== xdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;k;L))
==  (s1, s2:A.state, v:A.da(k). (s1  s2 mod x)  (f(s1,v) = f(s2,v))) 

latex

---

clarification:

M.rframe(A.effect f of k on y)
== IdIdDeqxdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;k;L))
==  (s1:A.state, s2:A.state, v:A.da(k).
==  ma-x-equiv(A;x;s1;s2)  (f(s1,v) = f(s2,v)  fpf-cap(A.1;IdDeq;y;Void))) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, t.2, P  Q, b, deq-member(eq;x;L), KindDeq, M.state, x:A. B(x), M.da(a), P  Q, (s1  s2 mod x), s = t, x:AB(x), , f(x)?z, t.1, IdDeq, Void, f(a)
FDL editor aliases	ma-rframe-ef